i:Id, ds:x:Id fp Type, x:Id, k:Knd, T:Type, test:(State(ds)T).
x  dom(ds)  R-base-recognize(i;ds;x;k;T;test)  Realizer 

latex

Definitions

t  T, Void, x:A. B(x), Top, Id, Type, IdDeq, f  g, f(x)?z, x:AB(x), x:A. B(x), State(ds), , x.A(x), x. t(x), x : v, DeclaredType(ds;x), f(a), true, if b t else f fi, @loc effect knd(v:T)  x := f State(ds) v , Knd, type List, nil, car.cdr, @loc only events in L change x:T, rec(x.A(x)), Realizer, false, @loc x initially v:T, left  right, R-base-recognize(i;ds;x;k;T;test), a:A fp B(a), x  dom(f), b, A, P  Q, False, {T}, SQType(T), s = t, Prop, s ~ t, x:AB(x), P & Q, P  Q, f(x), <a,b>, f || g, f  g

Lemmas

ma-state-subtype, fpf-sub-join-right, fpf-single-dom, Id sq, not wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf wf, Rplus wf, Rinit wf, bfalse wf, Rframe wf, Knd wf, Reffect wf, ifthenelse wf, decl-type wf, btrue wf, fpf-cap-single-join, fpf-cap wf, top wf, decl-state wf, fpf-join wf, fpf-single wf, Id wf, bool wf, id-deq wf